the_es:ES, j:E, m:Msg. isrcv(j)  haslink(lnk(j);m)  Type 

latex

Definitions	P  Q, x:A. B(x), lnk(e), t  T, mlnk(m), IdLnk, haslink(l;m), ES, E, Msg, isrcv(e), b
Lemmas	assert wf, es-isrcv wf, es-Msg wf, es-E wf, event system wf, IdLnk wf, mlnk wf2, es-lnk wf